with System.Storage_Elements;
use System.Storage_Elements;
package Storage_Streams.Binding is

   -- bind to specified memory address
   type Binding_Stream_Type is new Storage_Stream_Type with private;
   -- if new data writen to stream, 
   -- Length will grow if Write_Position > Length

   -- set writen length to zero
   overriding
   procedure Clear (this : in out Binding_Stream_Type) 
      with Post => this.Length = 0 
      and this.Read_Position = 1 
      and this.Write_Position = 1;

   overriding
   procedure Reset_For_Read (this : in out Binding_Stream_Type)
      with Post => this.Read_Position = 1;

   overriding
   procedure Reset_For_Write (this : in out Binding_Stream_Type)
      with Post => this.Write_Position = 1;

   overriding
   procedure Read (
      this : in out Binding_Stream_Type;
      Item : out Stream_Element_Array;
      Last : out Stream_Element_Offset
      );

   overriding
   procedure Write ( 
      this : in out Binding_Stream_Type;
      Item : Stream_Element_Array 
      );

   overriding
   function Read_Position (
      this : Binding_Stream_Type 
      ) return Stream_Element_Offset;

   overriding
   function Write_Position (
      this : Binding_Stream_Type 
      ) return Stream_Element_Offset;

   overriding
   procedure Set_Read_Position (
      this     : in out Binding_Stream_Type;
      Position : Stream_Element_Offset
      ) with Pre => Position in 1 .. this.Size;

   overriding
   procedure Set_Write_Position (
      this     : in out Binding_Stream_Type;
      Position : Stream_Element_Offset
      ) with Pre => Position in 1 .. this.Size;

   procedure Bind (
      this : in out Binding_Stream_Type;
      To   : System.Address;
      Size : Storage_Count
      ) with 
      Pre  => Size > 0,
      Post => this.Length = this.Size 
      and this.Read_Position = 1 and this.Write_Position = 1;

   function Size (
      this : Binding_Stream_Type'Class
      ) return Stream_Element_Count with Inline;

private

   type Binding_Stream_Type is new Storage_Stream_Type with record
      F_Address     : System.Address;
      F_Size        : Storage_Count;
      F_Read_Index  : Stream_Element_Offset := 1;
      F_Write_Index : Stream_Element_Offset := 1;
   end record;

end Storage_Streams.Binding;
